;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(require "mhelpers.lisp")

(module tHelpers
  (import iHelpers)
  (include-book "testing" :dir :teachpacks)
  (include-book "doublecheck" :dir :teachpacks) 
  
  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  ; SANITY CHECKS
  (check-expect (RGB-to-HSV 0 0 0) (list 0 0 0))
  (check-expect (HSV-to-RGB 0 0 0) (list 0 0 0))
  (check-expect (RGB-to-HSV 255 255 255) (list 0 0 255))
  (check-expect (HSV-to-RGB 360 1 255) (list 255 0 255))
  (check-expect (RGB-to-HSV 256 0 0) "Invalid RGB value.")
  (check-expect (HSV-to-RGB 361 0 0) "Invalid HSV value.")
  (check-expect (list 55 55 55)
                (let* ((hsv (RGB-to-HSV 55 55 55))
                       (h   (car hsv))
                       (s   (cadr hsv))
                       (v   (caddr hsv)))
                  (HSV-to-RGB h s v)))
  (check-expect (list 55 1 55)
                (let* ((rgb (HSV-to-RGB 55 1 55))
                       (r   (car rgb))
                       (g   (cadr rgb))
                       (b   (caddr rgb)))
                  (RGB-to-HSV r g b)))
  
  
  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  ; PROPERTIES
  ; RGB-to-HSV returns a list of three numbers:
  ; rational h [0, 360], rational s [0, 1], rational v [0, 255]
  (defproperty rgb-to-hsv-returns-list-of-3-prp
    (r :value (random-natural)
       :where (<= r 255)
     g :value (random-natural)
       :where (<= g 255)
     b :value (random-natural)
       :where (<= b 255))
    (let* ((hsv (RGB-to-HSV r g b))
           (h   (car hsv))
           (s   (cadr hsv))
           (v   (caddr hsv)))
      (and (and (consp hsv) (= (len hsv) 3))
           (and (natp h) (<= h 360))
           (and (rationalp s) (>= s 0) (<= s 1))
           (and (natp v) (<= v 255)))))
  
  ; HSV-to-RGB returns a list of three numbers between [0, 255]
  (defproperty hsv-to-rgb-returns-list-of-3-prp
    (h :value (random-natural)
       :where (<= h 360)
     s :value (random-rational)
       :where (and (<= s 1) (>= s 0))
     v :value (random-natural)
       :where (<= v 255))
    (let* ((rgb (HSV-to-RGB h s v))
           (r   (car rgb))
           (g   (cadr rgb))
           (b   (caddr rgb)))
      (and (and (consp rgb) (= (len rgb) 3))
           (and (natp r) (<= r 255))
           (and (natp g) (<= g 255))
           (and (natp b) (<= b 255)))))
  
  ; In the HSV color model, if value is 0,
  ; the color is black (R = 0, G = 0, B = 0).
  (defproperty hsv-to-rgb-0-v-is-black-prp
    (h :value (random-natural)
       :where (<= h 360)
     s :value (random-rational)
       :where (and (<= s 1) (>= s 0)))
    (equal (HSV-to-RGB h s 0) (list 0 0 0)))
  
  ; In the HSV color model, if value is 255 and saturation is 0,
  ; the color is white (R = 255, G = 255, B = 255).
  (defproperty hsv-to-rgb-255-v-and-0-s-is-white-prp
    (h :value (random-natural)
       :where (<= h 360))
    (equal (HSV-to-RGB h 0 255) (list 255 255 255)))
  
  ; In the HSV color model, if satuation is 0 and value is nonzero,
  ; the color is grey (R = x, G = x, B = x, where 0 <= x <= 255).
  (defproperty hsv-to-rgb-0-s-and-nonzero-v-is-grey-prp
    (h :value (random-natural)
       :where (<= h 360)
     v :value (random-natural)
       :where (<= v 255))
    (let* ((rgb (HSV-to-RGB h 0 v))
           (r   (car rgb))
           (g   (cadr rgb))
           (b   (caddr rgb)))
      (and (equal r g)
           (equal g b))))
  
  ; Using RGB-to-HSV and then HSV-to-RGB returns an approximate of the original values.
  ; In this case, the approximate is within 5 units (usually fewer) of the original rgb values.
  (defproperty rgb-to-hsv-approximates-hsv-to-rgb-prp
    (r :value (random-natural)
       :where (<= r 255)
     g :value (random-natural)
       :where (<= g 255)
     b :value (random-natural)
       :where (<= b 255))
    (let* ((hsv  (RGB-to-HSV r g b))
           (h    (car hsv))
           (s    (cadr hsv))
           (v    (caddr hsv))
           (rgb  (HSV-to-RGB h s v))
           (newR (car rgb))
           (newG (cadr rgb))
           (newB (caddr rgb)))
      (and (< (abs (- r newR)) 5)
           (< (abs (- g newG)) 5)
           (< (abs (- b newB)) 5))))
  
  ; Using HSV-to-RGB and then RGB-to-HSV returns the original value v.
  ; This is not true for hue and saturation due to the nature of the HSV color model.
  (defproperty hsv-to-rgb-then-rgb-to-hsv-reverses-v-prp
    (h :value (random-natural)
       :where (<= h 360)
     s :value (random-rational)
       :where (and (<= s 1) (>= s 0))
     v :value (random-natural)
       :where (<= v 255))
    (let* ((rgb  (HSV-to-RGB h s v))
           (r    (car rgb))
           (g    (cadr rgb))
           (b    (caddr rgb))
           (hsv  (RGB-to-HSV r g b))
           (newV (caddr hsv)))
      (equal newV v))))
  
(link rtHelpers (mHelpers tHelpers))
(invoke rtHelpers)